Inference at * 
Iof proof for Lemma before-hd:


  T:Type, L:(T List). (0 < ||L||)  no_repeats(T;L)  (x:T. x before hd(L)  L  False) 

latex

 by ((Auto) 
CollapseTHEN (((((InstLemma `no_repeats_iff` [T;L]) 
THENM (((ThinTrivial) 

THECollapseTHEN (Thin (-2)))))) 
TCollapseTHENA (Auto)))) 

latex

TC1: 

TC1: 1. T : Type
TC1: 2. L : T List
TC1: 3. 0 < ||L||
TC1: 4. no_repeats(T;L)
TC1: 5. x : T
TC1: 6. x before hd(L)  L
TC1: 7. x, y:T. x before y  L  ((x = y))
TC1:   False
TC.

Definitions	a < b, type List, Type, Void, ||as||, False, x:A. B(x), P  Q, P & Q, x:A  B(x), P  Q, P  Q, x:AB(x), x before y  l, no_repeats(T;l)
Lemmas	no repeats wf, l before wf, false wf, no repeats iff